Nuprl Lemma : rcv?-kind
11,40
postcript
pdf
E
,
X1
,
X2
:Type,
info
:(
E
((
:Id
X1
) + (
:(
:IdLnk
E
)
X2
))),
e
:
E
.
sqequal(rcv?(
e
); isrcv(kind(
e
)))
latex
Definitions
tt
,
ff
,
isrcv(
k
)
,
rcv(
l
,
tg
)
,
locl(
a
)
,
left
+
right
,
t
T
,
IdLnk
,
x
:
A
B
(
x
)
,
Id
,
f
(
a
)
,
x
:
A
B
(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
s
=
t
,
ecase1(
e
;
info
;
i
.
f
(
i
);
l
,
e'
.
g
(
l
;
e'
))
,
kind(
e
)
,
rcv?(
e
)
,
Type
,
<
a
,
b
>
,
,
guard(
T
)
,
sq_type(
T
)
,
sqequal(
s
;
t
)
Lemmas
bool
sq
,
Id
wf
,
IdLnk
wf
,
bfalse
wf
,
btrue
wf
origin
E,X1,X2:Type, info:(E
((:Id 
X1) + (:(:IdLnk E) X2))), e:E.
E,X1,X2:Type, info:(E((:Id X1) + (:(:IdLnk E) X2))), e:E.
T B(x)B(x)
Qx:A. B(x)